H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.785 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((succ :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(m,_)→m

is transformed to

m0 (m,_) = m

The following Lambda expression

\(_,r)→r

is transformed to

r0 (_,r) = r

The following Lambda expression

\(q,_)→q

is transformed to

q1 (q,_) = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Main

((succ :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Main

((succ :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Double vy vz)

is replaced by the following term

Double vy vz

The bind variable of the following binding Pattern

frac@(Float ww wx)

is replaced by the following term

Float ww wx

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((succ :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((succ :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

m

where

m = m0 vu6

m0 (m,vv) = m

vu6 = properFraction x

are unpacked to the following functions on top level

truncateM xw = truncateM0 xw (truncateVu6 xw)

truncateM0 xw (m,vv) = m

truncateVu6 xw = properFraction xw

The bindings of the following Let/Where expression

(fromIntegral q,r :% y)

where

q = q1 vu30

q1 (q,wz) = q

r = r0 vu30

r0 (xu,r) = r

vu30 = quotRem x y

are unpacked to the following functions on top level

properFractionVu30 xx xy = quotRem xx xy

properFractionR xx xy = properFractionR0 xx xy (properFractionVu30 xx xy)

properFractionQ1 xx xy (q,wz) = q

properFractionR0 xx xy (xu,r) = r

properFractionQ xx xy = properFractionQ1 xx xy (properFractionVu30 xx xy)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((succ :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(succ :: Float -> Float)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="succ",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="succ xz3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="toEnum . (Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="toEnum ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="primIntToFloat ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="Float ((Pos (Succ Zero) +) . fromEnum) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];7 -> 8[label="",style="dashed", color="green", weight=3];
8[label="(Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="Pos (Succ Zero) + fromEnum xz3",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="primPlusInt (Pos (Succ Zero)) (fromEnum xz3)",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="primPlusInt (Pos (Succ Zero)) (truncate xz3)",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="primPlusInt (Pos (Succ Zero)) (truncateM xz3)",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="primPlusInt (Pos (Succ Zero)) (truncateM0 xz3 (truncateVu6 xz3))",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="primPlusInt (Pos (Succ Zero)) (truncateM0 xz3 (properFraction xz3))",fontsize=16,color="black",shape="box"];14 -> 15[label="",style="solid", color="black", weight=3];
15[label="primPlusInt (Pos (Succ Zero)) (truncateM0 xz3 (floatProperFractionFloat xz3))",fontsize=16,color="burlywood",shape="box"];2381[label="xz3/Float xz30 xz31",fontsize=10,color="white",style="solid",shape="box"];15 -> 2381[label="",style="solid", color="burlywood", weight=9];
2381 -> 16[label="",style="solid", color="burlywood", weight=3];
16[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (Float xz30 xz31) (floatProperFractionFloat (Float xz30 xz31)))",fontsize=16,color="black",shape="box"];16 -> 17[label="",style="solid", color="black", weight=3];
17[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (Float xz30 xz31) (fromInt (xz30 `quot` xz31),Float xz30 xz31 - fromInt (xz30 `quot` xz31)))",fontsize=16,color="black",shape="box"];17 -> 18[label="",style="solid", color="black", weight=3];
18[label="primPlusInt (Pos (Succ Zero)) (fromInt (xz30 `quot` xz31))",fontsize=16,color="black",shape="box"];18 -> 19[label="",style="solid", color="black", weight=3];
19[label="primPlusInt (Pos (Succ Zero)) (xz30 `quot` xz31)",fontsize=16,color="black",shape="box"];19 -> 20[label="",style="solid", color="black", weight=3];
20[label="primPlusInt (Pos (Succ Zero)) (primQuotInt xz30 xz31)",fontsize=16,color="burlywood",shape="box"];2382[label="xz30/Pos xz300",fontsize=10,color="white",style="solid",shape="box"];20 -> 2382[label="",style="solid", color="burlywood", weight=9];
2382 -> 21[label="",style="solid", color="burlywood", weight=3];
2383[label="xz30/Neg xz300",fontsize=10,color="white",style="solid",shape="box"];20 -> 2383[label="",style="solid", color="burlywood", weight=9];
2383 -> 22[label="",style="solid", color="burlywood", weight=3];
21[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos xz300) xz31)",fontsize=16,color="burlywood",shape="box"];2384[label="xz31/Pos xz310",fontsize=10,color="white",style="solid",shape="box"];21 -> 2384[label="",style="solid", color="burlywood", weight=9];
2384 -> 23[label="",style="solid", color="burlywood", weight=3];
2385[label="xz31/Neg xz310",fontsize=10,color="white",style="solid",shape="box"];21 -> 2385[label="",style="solid", color="burlywood", weight=9];
2385 -> 24[label="",style="solid", color="burlywood", weight=3];
22[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg xz300) xz31)",fontsize=16,color="burlywood",shape="box"];2386[label="xz31/Pos xz310",fontsize=10,color="white",style="solid",shape="box"];22 -> 2386[label="",style="solid", color="burlywood", weight=9];
2386 -> 25[label="",style="solid", color="burlywood", weight=3];
2387[label="xz31/Neg xz310",fontsize=10,color="white",style="solid",shape="box"];22 -> 2387[label="",style="solid", color="burlywood", weight=9];
2387 -> 26[label="",style="solid", color="burlywood", weight=3];
23[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos xz300) (Pos xz310))",fontsize=16,color="burlywood",shape="box"];2388[label="xz310/Succ xz3100",fontsize=10,color="white",style="solid",shape="box"];23 -> 2388[label="",style="solid", color="burlywood", weight=9];
2388 -> 27[label="",style="solid", color="burlywood", weight=3];
2389[label="xz310/Zero",fontsize=10,color="white",style="solid",shape="box"];23 -> 2389[label="",style="solid", color="burlywood", weight=9];
2389 -> 28[label="",style="solid", color="burlywood", weight=3];
24[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos xz300) (Neg xz310))",fontsize=16,color="burlywood",shape="box"];2390[label="xz310/Succ xz3100",fontsize=10,color="white",style="solid",shape="box"];24 -> 2390[label="",style="solid", color="burlywood", weight=9];
2390 -> 29[label="",style="solid", color="burlywood", weight=3];
2391[label="xz310/Zero",fontsize=10,color="white",style="solid",shape="box"];24 -> 2391[label="",style="solid", color="burlywood", weight=9];
2391 -> 30[label="",style="solid", color="burlywood", weight=3];
25[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg xz300) (Pos xz310))",fontsize=16,color="burlywood",shape="box"];2392[label="xz310/Succ xz3100",fontsize=10,color="white",style="solid",shape="box"];25 -> 2392[label="",style="solid", color="burlywood", weight=9];
2392 -> 31[label="",style="solid", color="burlywood", weight=3];
2393[label="xz310/Zero",fontsize=10,color="white",style="solid",shape="box"];25 -> 2393[label="",style="solid", color="burlywood", weight=9];
2393 -> 32[label="",style="solid", color="burlywood", weight=3];
26[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg xz300) (Neg xz310))",fontsize=16,color="burlywood",shape="box"];2394[label="xz310/Succ xz3100",fontsize=10,color="white",style="solid",shape="box"];26 -> 2394[label="",style="solid", color="burlywood", weight=9];
2394 -> 33[label="",style="solid", color="burlywood", weight=3];
2395[label="xz310/Zero",fontsize=10,color="white",style="solid",shape="box"];26 -> 2395[label="",style="solid", color="burlywood", weight=9];
2395 -> 34[label="",style="solid", color="burlywood", weight=3];
27[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos xz300) (Pos (Succ xz3100)))",fontsize=16,color="black",shape="box"];27 -> 35[label="",style="solid", color="black", weight=3];
28[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos xz300) (Pos Zero))",fontsize=16,color="black",shape="box"];28 -> 36[label="",style="solid", color="black", weight=3];
29[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos xz300) (Neg (Succ xz3100)))",fontsize=16,color="black",shape="box"];29 -> 37[label="",style="solid", color="black", weight=3];
30[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos xz300) (Neg Zero))",fontsize=16,color="black",shape="box"];30 -> 38[label="",style="solid", color="black", weight=3];
31[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg xz300) (Pos (Succ xz3100)))",fontsize=16,color="black",shape="box"];31 -> 39[label="",style="solid", color="black", weight=3];
32[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg xz300) (Pos Zero))",fontsize=16,color="black",shape="box"];32 -> 40[label="",style="solid", color="black", weight=3];
33[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg xz300) (Neg (Succ xz3100)))",fontsize=16,color="black",shape="box"];33 -> 41[label="",style="solid", color="black", weight=3];
34[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg xz300) (Neg Zero))",fontsize=16,color="black",shape="box"];34 -> 42[label="",style="solid", color="black", weight=3];
35[label="primPlusInt (Pos (Succ Zero)) (Pos (primDivNatS xz300 (Succ xz3100)))",fontsize=16,color="black",shape="triangle"];35 -> 43[label="",style="solid", color="black", weight=3];
36[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="black",shape="triangle"];36 -> 44[label="",style="solid", color="black", weight=3];
37[label="primPlusInt (Pos (Succ Zero)) (Neg (primDivNatS xz300 (Succ xz3100)))",fontsize=16,color="black",shape="triangle"];37 -> 45[label="",style="solid", color="black", weight=3];
38 -> 36[label="",style="dashed", color="red", weight=0];
38[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="magenta"];39 -> 37[label="",style="dashed", color="red", weight=0];
39[label="primPlusInt (Pos (Succ Zero)) (Neg (primDivNatS xz300 (Succ xz3100)))",fontsize=16,color="magenta"];39 -> 46[label="",style="dashed", color="magenta", weight=3];
39 -> 47[label="",style="dashed", color="magenta", weight=3];
40 -> 36[label="",style="dashed", color="red", weight=0];
40[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="magenta"];41 -> 35[label="",style="dashed", color="red", weight=0];
41[label="primPlusInt (Pos (Succ Zero)) (Pos (primDivNatS xz300 (Succ xz3100)))",fontsize=16,color="magenta"];41 -> 48[label="",style="dashed", color="magenta", weight=3];
41 -> 49[label="",style="dashed", color="magenta", weight=3];
42 -> 36[label="",style="dashed", color="red", weight=0];
42[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="magenta"];43[label="Pos (primPlusNat (Succ Zero) (primDivNatS xz300 (Succ xz3100)))",fontsize=16,color="green",shape="box"];43 -> 50[label="",style="dashed", color="green", weight=3];
44[label="error []",fontsize=16,color="red",shape="box"];45[label="primMinusNat (Succ Zero) (primDivNatS xz300 (Succ xz3100))",fontsize=16,color="burlywood",shape="box"];2401[label="xz300/Succ xz3000",fontsize=10,color="white",style="solid",shape="box"];45 -> 2401[label="",style="solid", color="burlywood", weight=9];
2401 -> 51[label="",style="solid", color="burlywood", weight=3];
2402[label="xz300/Zero",fontsize=10,color="white",style="solid",shape="box"];45 -> 2402[label="",style="solid", color="burlywood", weight=9];
2402 -> 52[label="",style="solid", color="burlywood", weight=3];
46[label="xz300",fontsize=16,color="green",shape="box"];47[label="xz3100",fontsize=16,color="green",shape="box"];48[label="xz3100",fontsize=16,color="green",shape="box"];49[label="xz300",fontsize=16,color="green",shape="box"];50[label="primPlusNat (Succ Zero) (primDivNatS xz300 (Succ xz3100))",fontsize=16,color="burlywood",shape="box"];2403[label="xz300/Succ xz3000",fontsize=10,color="white",style="solid",shape="box"];50 -> 2403[label="",style="solid", color="burlywood", weight=9];
2403 -> 53[label="",style="solid", color="burlywood", weight=3];
2404[label="xz300/Zero",fontsize=10,color="white",style="solid",shape="box"];50 -> 2404[label="",style="solid", color="burlywood", weight=9];
2404 -> 54[label="",style="solid", color="burlywood", weight=3];
51[label="primMinusNat (Succ Zero) (primDivNatS (Succ xz3000) (Succ xz3100))",fontsize=16,color="black",shape="box"];51 -> 55[label="",style="solid", color="black", weight=3];
52[label="primMinusNat (Succ Zero) (primDivNatS Zero (Succ xz3100))",fontsize=16,color="black",shape="box"];52 -> 56[label="",style="solid", color="black", weight=3];
53[label="primPlusNat (Succ Zero) (primDivNatS (Succ xz3000) (Succ xz3100))",fontsize=16,color="black",shape="box"];53 -> 57[label="",style="solid", color="black", weight=3];
54[label="primPlusNat (Succ Zero) (primDivNatS Zero (Succ xz3100))",fontsize=16,color="black",shape="box"];54 -> 58[label="",style="solid", color="black", weight=3];
55[label="primMinusNat (Succ Zero) (primDivNatS0 xz3000 xz3100 (primGEqNatS xz3000 xz3100))",fontsize=16,color="burlywood",shape="box"];2405[label="xz3000/Succ xz30000",fontsize=10,color="white",style="solid",shape="box"];55 -> 2405[label="",style="solid", color="burlywood", weight=9];
2405 -> 59[label="",style="solid", color="burlywood", weight=3];
2406[label="xz3000/Zero",fontsize=10,color="white",style="solid",shape="box"];55 -> 2406[label="",style="solid", color="burlywood", weight=9];
2406 -> 60[label="",style="solid", color="burlywood", weight=3];
56[label="primMinusNat (Succ Zero) Zero",fontsize=16,color="black",shape="triangle"];56 -> 61[label="",style="solid", color="black", weight=3];
57[label="primPlusNat (Succ Zero) (primDivNatS0 xz3000 xz3100 (primGEqNatS xz3000 xz3100))",fontsize=16,color="burlywood",shape="box"];2407[label="xz3000/Succ xz30000",fontsize=10,color="white",style="solid",shape="box"];57 -> 2407[label="",style="solid", color="burlywood", weight=9];
2407 -> 62[label="",style="solid", color="burlywood", weight=3];
2408[label="xz3000/Zero",fontsize=10,color="white",style="solid",shape="box"];57 -> 2408[label="",style="solid", color="burlywood", weight=9];
2408 -> 63[label="",style="solid", color="burlywood", weight=3];
58[label="primPlusNat (Succ Zero) Zero",fontsize=16,color="black",shape="triangle"];58 -> 64[label="",style="solid", color="black", weight=3];
59[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz30000) xz3100 (primGEqNatS (Succ xz30000) xz3100))",fontsize=16,color="burlywood",shape="box"];2409[label="xz3100/Succ xz31000",fontsize=10,color="white",style="solid",shape="box"];59 -> 2409[label="",style="solid", color="burlywood", weight=9];
2409 -> 65[label="",style="solid", color="burlywood", weight=3];
2410[label="xz3100/Zero",fontsize=10,color="white",style="solid",shape="box"];59 -> 2410[label="",style="solid", color="burlywood", weight=9];
2410 -> 66[label="",style="solid", color="burlywood", weight=3];
60[label="primMinusNat (Succ Zero) (primDivNatS0 Zero xz3100 (primGEqNatS Zero xz3100))",fontsize=16,color="burlywood",shape="box"];2411[label="xz3100/Succ xz31000",fontsize=10,color="white",style="solid",shape="box"];60 -> 2411[label="",style="solid", color="burlywood", weight=9];
2411 -> 67[label="",style="solid", color="burlywood", weight=3];
2412[label="xz3100/Zero",fontsize=10,color="white",style="solid",shape="box"];60 -> 2412[label="",style="solid", color="burlywood", weight=9];
2412 -> 68[label="",style="solid", color="burlywood", weight=3];
61[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];62[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz30000) xz3100 (primGEqNatS (Succ xz30000) xz3100))",fontsize=16,color="burlywood",shape="box"];2413[label="xz3100/Succ xz31000",fontsize=10,color="white",style="solid",shape="box"];62 -> 2413[label="",style="solid", color="burlywood", weight=9];
2413 -> 69[label="",style="solid", color="burlywood", weight=3];
2414[label="xz3100/Zero",fontsize=10,color="white",style="solid",shape="box"];62 -> 2414[label="",style="solid", color="burlywood", weight=9];
2414 -> 70[label="",style="solid", color="burlywood", weight=3];
63[label="primPlusNat (Succ Zero) (primDivNatS0 Zero xz3100 (primGEqNatS Zero xz3100))",fontsize=16,color="burlywood",shape="box"];2415[label="xz3100/Succ xz31000",fontsize=10,color="white",style="solid",shape="box"];63 -> 2415[label="",style="solid", color="burlywood", weight=9];
2415 -> 71[label="",style="solid", color="burlywood", weight=3];
2416[label="xz3100/Zero",fontsize=10,color="white",style="solid",shape="box"];63 -> 2416[label="",style="solid", color="burlywood", weight=9];
2416 -> 72[label="",style="solid", color="burlywood", weight=3];
64[label="Succ Zero",fontsize=16,color="green",shape="box"];65[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz30000) (Succ xz31000) (primGEqNatS (Succ xz30000) (Succ xz31000)))",fontsize=16,color="black",shape="box"];65 -> 73[label="",style="solid", color="black", weight=3];
66[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz30000) Zero (primGEqNatS (Succ xz30000) Zero))",fontsize=16,color="black",shape="box"];66 -> 74[label="",style="solid", color="black", weight=3];
67[label="primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ xz31000) (primGEqNatS Zero (Succ xz31000)))",fontsize=16,color="black",shape="box"];67 -> 75[label="",style="solid", color="black", weight=3];
68[label="primMinusNat (Succ Zero) (primDivNatS0 Zero Zero (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];68 -> 76[label="",style="solid", color="black", weight=3];
69[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz30000) (Succ xz31000) (primGEqNatS (Succ xz30000) (Succ xz31000)))",fontsize=16,color="black",shape="box"];69 -> 77[label="",style="solid", color="black", weight=3];
70[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz30000) Zero (primGEqNatS (Succ xz30000) Zero))",fontsize=16,color="black",shape="box"];70 -> 78[label="",style="solid", color="black", weight=3];
71[label="primPlusNat (Succ Zero) (primDivNatS0 Zero (Succ xz31000) (primGEqNatS Zero (Succ xz31000)))",fontsize=16,color="black",shape="box"];71 -> 79[label="",style="solid", color="black", weight=3];
72[label="primPlusNat (Succ Zero) (primDivNatS0 Zero Zero (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];72 -> 80[label="",style="solid", color="black", weight=3];
73 -> 684[label="",style="dashed", color="red", weight=0];
73[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz30000) (Succ xz31000) (primGEqNatS xz30000 xz31000))",fontsize=16,color="magenta"];73 -> 685[label="",style="dashed", color="magenta", weight=3];
73 -> 686[label="",style="dashed", color="magenta", weight=3];
73 -> 687[label="",style="dashed", color="magenta", weight=3];
73 -> 688[label="",style="dashed", color="magenta", weight=3];
74[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz30000) Zero True)",fontsize=16,color="black",shape="box"];74 -> 83[label="",style="solid", color="black", weight=3];
75[label="primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ xz31000) False)",fontsize=16,color="black",shape="box"];75 -> 84[label="",style="solid", color="black", weight=3];
76[label="primMinusNat (Succ Zero) (primDivNatS0 Zero Zero True)",fontsize=16,color="black",shape="box"];76 -> 85[label="",style="solid", color="black", weight=3];
77 -> 727[label="",style="dashed", color="red", weight=0];
77[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz30000) (Succ xz31000) (primGEqNatS xz30000 xz31000))",fontsize=16,color="magenta"];77 -> 728[label="",style="dashed", color="magenta", weight=3];
77 -> 729[label="",style="dashed", color="magenta", weight=3];
77 -> 730[label="",style="dashed", color="magenta", weight=3];
77 -> 731[label="",style="dashed", color="magenta", weight=3];
78[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz30000) Zero True)",fontsize=16,color="black",shape="box"];78 -> 88[label="",style="solid", color="black", weight=3];
79[label="primPlusNat (Succ Zero) (primDivNatS0 Zero (Succ xz31000) False)",fontsize=16,color="black",shape="box"];79 -> 89[label="",style="solid", color="black", weight=3];
80[label="primPlusNat (Succ Zero) (primDivNatS0 Zero Zero True)",fontsize=16,color="black",shape="box"];80 -> 90[label="",style="solid", color="black", weight=3];
685[label="xz31000",fontsize=16,color="green",shape="box"];686[label="xz30000",fontsize=16,color="green",shape="box"];687[label="xz30000",fontsize=16,color="green",shape="box"];688[label="xz31000",fontsize=16,color="green",shape="box"];684[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS xz47 xz48))",fontsize=16,color="burlywood",shape="triangle"];2419[label="xz47/Succ xz470",fontsize=10,color="white",style="solid",shape="box"];684 -> 2419[label="",style="solid", color="burlywood", weight=9];
2419 -> 725[label="",style="solid", color="burlywood", weight=3];
2420[label="xz47/Zero",fontsize=10,color="white",style="solid",shape="box"];684 -> 2420[label="",style="solid", color="burlywood", weight=9];
2420 -> 726[label="",style="solid", color="burlywood", weight=3];
83[label="primMinusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS (Succ xz30000) Zero) (Succ Zero)))",fontsize=16,color="black",shape="box"];83 -> 95[label="",style="solid", color="black", weight=3];
84 -> 56[label="",style="dashed", color="red", weight=0];
84[label="primMinusNat (Succ Zero) Zero",fontsize=16,color="magenta"];85[label="primMinusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)))",fontsize=16,color="black",shape="box"];85 -> 96[label="",style="solid", color="black", weight=3];
728[label="xz30000",fontsize=16,color="green",shape="box"];729[label="xz31000",fontsize=16,color="green",shape="box"];730[label="xz31000",fontsize=16,color="green",shape="box"];731[label="xz30000",fontsize=16,color="green",shape="box"];727[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS xz52 xz53))",fontsize=16,color="burlywood",shape="triangle"];2422[label="xz52/Succ xz520",fontsize=10,color="white",style="solid",shape="box"];727 -> 2422[label="",style="solid", color="burlywood", weight=9];
2422 -> 768[label="",style="solid", color="burlywood", weight=3];
2423[label="xz52/Zero",fontsize=10,color="white",style="solid",shape="box"];727 -> 2423[label="",style="solid", color="burlywood", weight=9];
2423 -> 769[label="",style="solid", color="burlywood", weight=3];
88[label="primPlusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS (Succ xz30000) Zero) (Succ Zero)))",fontsize=16,color="black",shape="box"];88 -> 101[label="",style="solid", color="black", weight=3];
89 -> 58[label="",style="dashed", color="red", weight=0];
89[label="primPlusNat (Succ Zero) Zero",fontsize=16,color="magenta"];90[label="primPlusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)))",fontsize=16,color="black",shape="box"];90 -> 102[label="",style="solid", color="black", weight=3];
725[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS (Succ xz470) xz48))",fontsize=16,color="burlywood",shape="box"];2425[label="xz48/Succ xz480",fontsize=10,color="white",style="solid",shape="box"];725 -> 2425[label="",style="solid", color="burlywood", weight=9];
2425 -> 770[label="",style="solid", color="burlywood", weight=3];
2426[label="xz48/Zero",fontsize=10,color="white",style="solid",shape="box"];725 -> 2426[label="",style="solid", color="burlywood", weight=9];
2426 -> 771[label="",style="solid", color="burlywood", weight=3];
726[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS Zero xz48))",fontsize=16,color="burlywood",shape="box"];2427[label="xz48/Succ xz480",fontsize=10,color="white",style="solid",shape="box"];726 -> 2427[label="",style="solid", color="burlywood", weight=9];
2427 -> 772[label="",style="solid", color="burlywood", weight=3];
2428[label="xz48/Zero",fontsize=10,color="white",style="solid",shape="box"];726 -> 2428[label="",style="solid", color="burlywood", weight=9];
2428 -> 773[label="",style="solid", color="burlywood", weight=3];
95 -> 1187[label="",style="dashed", color="red", weight=0];
95[label="primMinusNat Zero (primDivNatS (primMinusNatS (Succ xz30000) Zero) (Succ Zero))",fontsize=16,color="magenta"];95 -> 1188[label="",style="dashed", color="magenta", weight=3];
95 -> 1189[label="",style="dashed", color="magenta", weight=3];
95 -> 1190[label="",style="dashed", color="magenta", weight=3];
96 -> 1187[label="",style="dashed", color="red", weight=0];
96[label="primMinusNat Zero (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="magenta"];96 -> 1191[label="",style="dashed", color="magenta", weight=3];
96 -> 1192[label="",style="dashed", color="magenta", weight=3];
96 -> 1193[label="",style="dashed", color="magenta", weight=3];
768[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS (Succ xz520) xz53))",fontsize=16,color="burlywood",shape="box"];2431[label="xz53/Succ xz530",fontsize=10,color="white",style="solid",shape="box"];768 -> 2431[label="",style="solid", color="burlywood", weight=9];
2431 -> 774[label="",style="solid", color="burlywood", weight=3];
2432[label="xz53/Zero",fontsize=10,color="white",style="solid",shape="box"];768 -> 2432[label="",style="solid", color="burlywood", weight=9];
2432 -> 775[label="",style="solid", color="burlywood", weight=3];
769[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS Zero xz53))",fontsize=16,color="burlywood",shape="box"];2433[label="xz53/Succ xz530",fontsize=10,color="white",style="solid",shape="box"];769 -> 2433[label="",style="solid", color="burlywood", weight=9];
2433 -> 776[label="",style="solid", color="burlywood", weight=3];
2434[label="xz53/Zero",fontsize=10,color="white",style="solid",shape="box"];769 -> 2434[label="",style="solid", color="burlywood", weight=9];
2434 -> 777[label="",style="solid", color="burlywood", weight=3];
101[label="Succ (Succ (primPlusNat Zero (primDivNatS (primMinusNatS (Succ xz30000) Zero) (Succ Zero))))",fontsize=16,color="green",shape="box"];101 -> 113[label="",style="dashed", color="green", weight=3];
102[label="Succ (Succ (primPlusNat Zero (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))))",fontsize=16,color="green",shape="box"];102 -> 114[label="",style="dashed", color="green", weight=3];
770[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS (Succ xz470) (Succ xz480)))",fontsize=16,color="black",shape="box"];770 -> 778[label="",style="solid", color="black", weight=3];
771[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS (Succ xz470) Zero))",fontsize=16,color="black",shape="box"];771 -> 779[label="",style="solid", color="black", weight=3];
772[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS Zero (Succ xz480)))",fontsize=16,color="black",shape="box"];772 -> 780[label="",style="solid", color="black", weight=3];
773[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];773 -> 781[label="",style="solid", color="black", weight=3];
1188[label="Zero",fontsize=16,color="green",shape="box"];1189[label="Succ xz30000",fontsize=16,color="green",shape="box"];1190[label="Zero",fontsize=16,color="green",shape="box"];1187[label="primMinusNat Zero (primDivNatS (primMinusNatS xz57 xz58) (Succ xz59))",fontsize=16,color="burlywood",shape="triangle"];2435[label="xz57/Succ xz570",fontsize=10,color="white",style="solid",shape="box"];1187 -> 2435[label="",style="solid", color="burlywood", weight=9];
2435 -> 1221[label="",style="solid", color="burlywood", weight=3];
2436[label="xz57/Zero",fontsize=10,color="white",style="solid",shape="box"];1187 -> 2436[label="",style="solid", color="burlywood", weight=9];
2436 -> 1222[label="",style="solid", color="burlywood", weight=3];
1191[label="Zero",fontsize=16,color="green",shape="box"];1192[label="Zero",fontsize=16,color="green",shape="box"];1193[label="Zero",fontsize=16,color="green",shape="box"];774[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS (Succ xz520) (Succ xz530)))",fontsize=16,color="black",shape="box"];774 -> 782[label="",style="solid", color="black", weight=3];
775[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS (Succ xz520) Zero))",fontsize=16,color="black",shape="box"];775 -> 783[label="",style="solid", color="black", weight=3];
776[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS Zero (Succ xz530)))",fontsize=16,color="black",shape="box"];776 -> 784[label="",style="solid", color="black", weight=3];
777[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];777 -> 785[label="",style="solid", color="black", weight=3];
113 -> 1242[label="",style="dashed", color="red", weight=0];
113[label="primPlusNat Zero (primDivNatS (primMinusNatS (Succ xz30000) Zero) (Succ Zero))",fontsize=16,color="magenta"];113 -> 1243[label="",style="dashed", color="magenta", weight=3];
113 -> 1244[label="",style="dashed", color="magenta", weight=3];
113 -> 1245[label="",style="dashed", color="magenta", weight=3];
114 -> 1242[label="",style="dashed", color="red", weight=0];
114[label="primPlusNat Zero (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="magenta"];114 -> 1246[label="",style="dashed", color="magenta", weight=3];
114 -> 1247[label="",style="dashed", color="magenta", weight=3];
114 -> 1248[label="",style="dashed", color="magenta", weight=3];
778 -> 684[label="",style="dashed", color="red", weight=0];
778[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) (primGEqNatS xz470 xz480))",fontsize=16,color="magenta"];778 -> 786[label="",style="dashed", color="magenta", weight=3];
778 -> 787[label="",style="dashed", color="magenta", weight=3];
779[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) True)",fontsize=16,color="black",shape="triangle"];779 -> 788[label="",style="solid", color="black", weight=3];
780[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) False)",fontsize=16,color="black",shape="box"];780 -> 789[label="",style="solid", color="black", weight=3];
781 -> 779[label="",style="dashed", color="red", weight=0];
781[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ xz45) (Succ xz46) True)",fontsize=16,color="magenta"];1221[label="primMinusNat Zero (primDivNatS (primMinusNatS (Succ xz570) xz58) (Succ xz59))",fontsize=16,color="burlywood",shape="box"];2441[label="xz58/Succ xz580",fontsize=10,color="white",style="solid",shape="box"];1221 -> 2441[label="",style="solid", color="burlywood", weight=9];
2441 -> 1238[label="",style="solid", color="burlywood", weight=3];
2442[label="xz58/Zero",fontsize=10,color="white",style="solid",shape="box"];1221 -> 2442[label="",style="solid", color="burlywood", weight=9];
2442 -> 1239[label="",style="solid", color="burlywood", weight=3];
1222[label="primMinusNat Zero (primDivNatS (primMinusNatS Zero xz58) (Succ xz59))",fontsize=16,color="burlywood",shape="box"];2443[label="xz58/Succ xz580",fontsize=10,color="white",style="solid",shape="box"];1222 -> 2443[label="",style="solid", color="burlywood", weight=9];
2443 -> 1240[label="",style="solid", color="burlywood", weight=3];
2444[label="xz58/Zero",fontsize=10,color="white",style="solid",shape="box"];1222 -> 2444[label="",style="solid", color="burlywood", weight=9];
2444 -> 1241[label="",style="solid", color="burlywood", weight=3];
782 -> 727[label="",style="dashed", color="red", weight=0];
782[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) (primGEqNatS xz520 xz530))",fontsize=16,color="magenta"];782 -> 790[label="",style="dashed", color="magenta", weight=3];
782 -> 791[label="",style="dashed", color="magenta", weight=3];
783[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) True)",fontsize=16,color="black",shape="triangle"];783 -> 792[label="",style="solid", color="black", weight=3];
784[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) False)",fontsize=16,color="black",shape="box"];784 -> 793[label="",style="solid", color="black", weight=3];
785 -> 783[label="",style="dashed", color="red", weight=0];
785[label="primPlusNat (Succ Zero) (primDivNatS0 (Succ xz50) (Succ xz51) True)",fontsize=16,color="magenta"];1243[label="Zero",fontsize=16,color="green",shape="box"];1244[label="Zero",fontsize=16,color="green",shape="box"];1245[label="Succ xz30000",fontsize=16,color="green",shape="box"];1242[label="primPlusNat Zero (primDivNatS (primMinusNatS xz61 xz62) (Succ xz63))",fontsize=16,color="burlywood",shape="triangle"];2447[label="xz61/Succ xz610",fontsize=10,color="white",style="solid",shape="box"];1242 -> 2447[label="",style="solid", color="burlywood", weight=9];
2447 -> 1276[label="",style="solid", color="burlywood", weight=3];
2448[label="xz61/Zero",fontsize=10,color="white",style="solid",shape="box"];1242 -> 2448[label="",style="solid", color="burlywood", weight=9];
2448 -> 1277[label="",style="solid", color="burlywood", weight=3];
1246[label="Zero",fontsize=16,color="green",shape="box"];1247[label="Zero",fontsize=16,color="green",shape="box"];1248[label="Zero",fontsize=16,color="green",shape="box"];786[label="xz480",fontsize=16,color="green",shape="box"];787[label="xz470",fontsize=16,color="green",shape="box"];788[label="primMinusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS (Succ xz45) (Succ xz46)) (Succ (Succ xz46))))",fontsize=16,color="black",shape="box"];788 -> 794[label="",style="solid", color="black", weight=3];
789 -> 56[label="",style="dashed", color="red", weight=0];
789[label="primMinusNat (Succ Zero) Zero",fontsize=16,color="magenta"];1238[label="primMinusNat Zero (primDivNatS (primMinusNatS (Succ xz570) (Succ xz580)) (Succ xz59))",fontsize=16,color="black",shape="box"];1238 -> 1278[label="",style="solid", color="black", weight=3];
1239[label="primMinusNat Zero (primDivNatS (primMinusNatS (Succ xz570) Zero) (Succ xz59))",fontsize=16,color="black",shape="box"];1239 -> 1279[label="",style="solid", color="black", weight=3];
1240[label="primMinusNat Zero (primDivNatS (primMinusNatS Zero (Succ xz580)) (Succ xz59))",fontsize=16,color="black",shape="box"];1240 -> 1280[label="",style="solid", color="black", weight=3];
1241[label="primMinusNat Zero (primDivNatS (primMinusNatS Zero Zero) (Succ xz59))",fontsize=16,color="black",shape="box"];1241 -> 1281[label="",style="solid", color="black", weight=3];
790[label="xz530",fontsize=16,color="green",shape="box"];791[label="xz520",fontsize=16,color="green",shape="box"];792[label="primPlusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS (Succ xz50) (Succ xz51)) (Succ (Succ xz51))))",fontsize=16,color="black",shape="box"];792 -> 795[label="",style="solid", color="black", weight=3];
793 -> 58[label="",style="dashed", color="red", weight=0];
793[label="primPlusNat (Succ Zero) Zero",fontsize=16,color="magenta"];1276[label="primPlusNat Zero (primDivNatS (primMinusNatS (Succ xz610) xz62) (Succ xz63))",fontsize=16,color="burlywood",shape="box"];2451[label="xz62/Succ xz620",fontsize=10,color="white",style="solid",shape="box"];1276 -> 2451[label="",style="solid", color="burlywood", weight=9];
2451 -> 1282[label="",style="solid", color="burlywood", weight=3];
2452[label="xz62/Zero",fontsize=10,color="white",style="solid",shape="box"];1276 -> 2452[label="",style="solid", color="burlywood", weight=9];
2452 -> 1283[label="",style="solid", color="burlywood", weight=3];
1277[label="primPlusNat Zero (primDivNatS (primMinusNatS Zero xz62) (Succ xz63))",fontsize=16,color="burlywood",shape="box"];2453[label="xz62/Succ xz620",fontsize=10,color="white",style="solid",shape="box"];1277 -> 2453[label="",style="solid", color="burlywood", weight=9];
2453 -> 1284[label="",style="solid", color="burlywood", weight=3];
2454[label="xz62/Zero",fontsize=10,color="white",style="solid",shape="box"];1277 -> 2454[label="",style="solid", color="burlywood", weight=9];
2454 -> 1285[label="",style="solid", color="burlywood", weight=3];
794 -> 1187[label="",style="dashed", color="red", weight=0];
794[label="primMinusNat Zero (primDivNatS (primMinusNatS (Succ xz45) (Succ xz46)) (Succ (Succ xz46)))",fontsize=16,color="magenta"];794 -> 1194[label="",style="dashed", color="magenta", weight=3];
794 -> 1195[label="",style="dashed", color="magenta", weight=3];
794 -> 1196[label="",style="dashed", color="magenta", weight=3];
1278 -> 1187[label="",style="dashed", color="red", weight=0];
1278[label="primMinusNat Zero (primDivNatS (primMinusNatS xz570 xz580) (Succ xz59))",fontsize=16,color="magenta"];1278 -> 1286[label="",style="dashed", color="magenta", weight=3];
1278 -> 1287[label="",style="dashed", color="magenta", weight=3];
1279[label="primMinusNat Zero (primDivNatS (Succ xz570) (Succ xz59))",fontsize=16,color="black",shape="box"];1279 -> 1288[label="",style="solid", color="black", weight=3];
1280[label="primMinusNat Zero (primDivNatS Zero (Succ xz59))",fontsize=16,color="black",shape="triangle"];1280 -> 1289[label="",style="solid", color="black", weight=3];
1281 -> 1280[label="",style="dashed", color="red", weight=0];
1281[label="primMinusNat Zero (primDivNatS Zero (Succ xz59))",fontsize=16,color="magenta"];795[label="Succ (Succ (primPlusNat Zero (primDivNatS (primMinusNatS (Succ xz50) (Succ xz51)) (Succ (Succ xz51)))))",fontsize=16,color="green",shape="box"];795 -> 797[label="",style="dashed", color="green", weight=3];
1282[label="primPlusNat Zero (primDivNatS (primMinusNatS (Succ xz610) (Succ xz620)) (Succ xz63))",fontsize=16,color="black",shape="box"];1282 -> 1290[label="",style="solid", color="black", weight=3];
1283[label="primPlusNat Zero (primDivNatS (primMinusNatS (Succ xz610) Zero) (Succ xz63))",fontsize=16,color="black",shape="box"];1283 -> 1291[label="",style="solid", color="black", weight=3];
1284[label="primPlusNat Zero (primDivNatS (primMinusNatS Zero (Succ xz620)) (Succ xz63))",fontsize=16,color="black",shape="box"];1284 -> 1292[label="",style="solid", color="black", weight=3];
1285[label="primPlusNat Zero (primDivNatS (primMinusNatS Zero Zero) (Succ xz63))",fontsize=16,color="black",shape="box"];1285 -> 1293[label="",style="solid", color="black", weight=3];
1194[label="Succ xz46",fontsize=16,color="green",shape="box"];1195[label="Succ xz45",fontsize=16,color="green",shape="box"];1196[label="Succ xz46",fontsize=16,color="green",shape="box"];1286[label="xz580",fontsize=16,color="green",shape="box"];1287[label="xz570",fontsize=16,color="green",shape="box"];1288[label="primMinusNat Zero (primDivNatS0 xz570 xz59 (primGEqNatS xz570 xz59))",fontsize=16,color="burlywood",shape="box"];2458[label="xz570/Succ xz5700",fontsize=10,color="white",style="solid",shape="box"];1288 -> 2458[label="",style="solid", color="burlywood", weight=9];
2458 -> 1294[label="",style="solid", color="burlywood", weight=3];
2459[label="xz570/Zero",fontsize=10,color="white",style="solid",shape="box"];1288 -> 2459[label="",style="solid", color="burlywood", weight=9];
2459 -> 1295[label="",style="solid", color="burlywood", weight=3];
1289[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="triangle"];1289 -> 1296[label="",style="solid", color="black", weight=3];
797 -> 1242[label="",style="dashed", color="red", weight=0];
797[label="primPlusNat Zero (primDivNatS (primMinusNatS (Succ xz50) (Succ xz51)) (Succ (Succ xz51)))",fontsize=16,color="magenta"];797 -> 1249[label="",style="dashed", color="magenta", weight=3];
797 -> 1250[label="",style="dashed", color="magenta", weight=3];
797 -> 1251[label="",style="dashed", color="magenta", weight=3];
1290 -> 1242[label="",style="dashed", color="red", weight=0];
1290[label="primPlusNat Zero (primDivNatS (primMinusNatS xz610 xz620) (Succ xz63))",fontsize=16,color="magenta"];1290 -> 1297[label="",style="dashed", color="magenta", weight=3];
1290 -> 1298[label="",style="dashed", color="magenta", weight=3];
1291[label="primPlusNat Zero (primDivNatS (Succ xz610) (Succ xz63))",fontsize=16,color="black",shape="box"];1291 -> 1299[label="",style="solid", color="black", weight=3];
1292[label="primPlusNat Zero (primDivNatS Zero (Succ xz63))",fontsize=16,color="black",shape="triangle"];1292 -> 1300[label="",style="solid", color="black", weight=3];
1293 -> 1292[label="",style="dashed", color="red", weight=0];
1293[label="primPlusNat Zero (primDivNatS Zero (Succ xz63))",fontsize=16,color="magenta"];1294[label="primMinusNat Zero (primDivNatS0 (Succ xz5700) xz59 (primGEqNatS (Succ xz5700) xz59))",fontsize=16,color="burlywood",shape="box"];2463[label="xz59/Succ xz590",fontsize=10,color="white",style="solid",shape="box"];1294 -> 2463[label="",style="solid", color="burlywood", weight=9];
2463 -> 1301[label="",style="solid", color="burlywood", weight=3];
2464[label="xz59/Zero",fontsize=10,color="white",style="solid",shape="box"];1294 -> 2464[label="",style="solid", color="burlywood", weight=9];
2464 -> 1302[label="",style="solid", color="burlywood", weight=3];
1295[label="primMinusNat Zero (primDivNatS0 Zero xz59 (primGEqNatS Zero xz59))",fontsize=16,color="burlywood",shape="box"];2465[label="xz59/Succ xz590",fontsize=10,color="white",style="solid",shape="box"];1295 -> 2465[label="",style="solid", color="burlywood", weight=9];
2465 -> 1303[label="",style="solid", color="burlywood", weight=3];
2466[label="xz59/Zero",fontsize=10,color="white",style="solid",shape="box"];1295 -> 2466[label="",style="solid", color="burlywood", weight=9];
2466 -> 1304[label="",style="solid", color="burlywood", weight=3];
1296[label="Pos Zero",fontsize=16,color="green",shape="box"];1249[label="Succ xz51",fontsize=16,color="green",shape="box"];1250[label="Succ xz51",fontsize=16,color="green",shape="box"];1251[label="Succ xz50",fontsize=16,color="green",shape="box"];1297[label="xz620",fontsize=16,color="green",shape="box"];1298[label="xz610",fontsize=16,color="green",shape="box"];1299[label="primPlusNat Zero (primDivNatS0 xz610 xz63 (primGEqNatS xz610 xz63))",fontsize=16,color="burlywood",shape="box"];2467[label="xz610/Succ xz6100",fontsize=10,color="white",style="solid",shape="box"];1299 -> 2467[label="",style="solid", color="burlywood", weight=9];
2467 -> 1305[label="",style="solid", color="burlywood", weight=3];
2468[label="xz610/Zero",fontsize=10,color="white",style="solid",shape="box"];1299 -> 2468[label="",style="solid", color="burlywood", weight=9];
2468 -> 1306[label="",style="solid", color="burlywood", weight=3];
1300[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="triangle"];1300 -> 1307[label="",style="solid", color="black", weight=3];
1301[label="primMinusNat Zero (primDivNatS0 (Succ xz5700) (Succ xz590) (primGEqNatS (Succ xz5700) (Succ xz590)))",fontsize=16,color="black",shape="box"];1301 -> 1308[label="",style="solid", color="black", weight=3];
1302[label="primMinusNat Zero (primDivNatS0 (Succ xz5700) Zero (primGEqNatS (Succ xz5700) Zero))",fontsize=16,color="black",shape="box"];1302 -> 1309[label="",style="solid", color="black", weight=3];
1303[label="primMinusNat Zero (primDivNatS0 Zero (Succ xz590) (primGEqNatS Zero (Succ xz590)))",fontsize=16,color="black",shape="box"];1303 -> 1310[label="",style="solid", color="black", weight=3];
1304[label="primMinusNat Zero (primDivNatS0 Zero Zero (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];1304 -> 1311[label="",style="solid", color="black", weight=3];
1305[label="primPlusNat Zero (primDivNatS0 (Succ xz6100) xz63 (primGEqNatS (Succ xz6100) xz63))",fontsize=16,color="burlywood",shape="box"];2469[label="xz63/Succ xz630",fontsize=10,color="white",style="solid",shape="box"];1305 -> 2469[label="",style="solid", color="burlywood", weight=9];
2469 -> 1312[label="",style="solid", color="burlywood", weight=3];
2470[label="xz63/Zero",fontsize=10,color="white",style="solid",shape="box"];1305 -> 2470[label="",style="solid", color="burlywood", weight=9];
2470 -> 1313[label="",style="solid", color="burlywood", weight=3];
1306[label="primPlusNat Zero (primDivNatS0 Zero xz63 (primGEqNatS Zero xz63))",fontsize=16,color="burlywood",shape="box"];2471[label="xz63/Succ xz630",fontsize=10,color="white",style="solid",shape="box"];1306 -> 2471[label="",style="solid", color="burlywood", weight=9];
2471 -> 1314[label="",style="solid", color="burlywood", weight=3];
2472[label="xz63/Zero",fontsize=10,color="white",style="solid",shape="box"];1306 -> 2472[label="",style="solid", color="burlywood", weight=9];
2472 -> 1315[label="",style="solid", color="burlywood", weight=3];
1307[label="Zero",fontsize=16,color="green",shape="box"];1308 -> 1871[label="",style="dashed", color="red", weight=0];
1308[label="primMinusNat Zero (primDivNatS0 (Succ xz5700) (Succ xz590) (primGEqNatS xz5700 xz590))",fontsize=16,color="magenta"];1308 -> 1872[label="",style="dashed", color="magenta", weight=3];
1308 -> 1873[label="",style="dashed", color="magenta", weight=3];
1308 -> 1874[label="",style="dashed", color="magenta", weight=3];
1308 -> 1875[label="",style="dashed", color="magenta", weight=3];
1309[label="primMinusNat Zero (primDivNatS0 (Succ xz5700) Zero True)",fontsize=16,color="black",shape="box"];1309 -> 1318[label="",style="solid", color="black", weight=3];
1310[label="primMinusNat Zero (primDivNatS0 Zero (Succ xz590) False)",fontsize=16,color="black",shape="box"];1310 -> 1319[label="",style="solid", color="black", weight=3];
1311[label="primMinusNat Zero (primDivNatS0 Zero Zero True)",fontsize=16,color="black",shape="box"];1311 -> 1320[label="",style="solid", color="black", weight=3];
1312[label="primPlusNat Zero (primDivNatS0 (Succ xz6100) (Succ xz630) (primGEqNatS (Succ xz6100) (Succ xz630)))",fontsize=16,color="black",shape="box"];1312 -> 1321[label="",style="solid", color="black", weight=3];
1313[label="primPlusNat Zero (primDivNatS0 (Succ xz6100) Zero (primGEqNatS (Succ xz6100) Zero))",fontsize=16,color="black",shape="box"];1313 -> 1322[label="",style="solid", color="black", weight=3];
1314[label="primPlusNat Zero (primDivNatS0 Zero (Succ xz630) (primGEqNatS Zero (Succ xz630)))",fontsize=16,color="black",shape="box"];1314 -> 1323[label="",style="solid", color="black", weight=3];
1315[label="primPlusNat Zero (primDivNatS0 Zero Zero (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];1315 -> 1324[label="",style="solid", color="black", weight=3];
1872[label="xz590",fontsize=16,color="green",shape="box"];1873[label="xz5700",fontsize=16,color="green",shape="box"];1874[label="xz590",fontsize=16,color="green",shape="box"];1875[label="xz5700",fontsize=16,color="green",shape="box"];1871[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS xz96 xz97))",fontsize=16,color="burlywood",shape="triangle"];2474[label="xz96/Succ xz960",fontsize=10,color="white",style="solid",shape="box"];1871 -> 2474[label="",style="solid", color="burlywood", weight=9];
2474 -> 1912[label="",style="solid", color="burlywood", weight=3];
2475[label="xz96/Zero",fontsize=10,color="white",style="solid",shape="box"];1871 -> 2475[label="",style="solid", color="burlywood", weight=9];
2475 -> 1913[label="",style="solid", color="burlywood", weight=3];
1318 -> 1677[label="",style="dashed", color="red", weight=0];
1318[label="primMinusNat Zero (Succ (primDivNatS (primMinusNatS (Succ xz5700) Zero) (Succ Zero)))",fontsize=16,color="magenta"];1318 -> 1678[label="",style="dashed", color="magenta", weight=3];
1319 -> 1289[label="",style="dashed", color="red", weight=0];
1319[label="primMinusNat Zero Zero",fontsize=16,color="magenta"];1320 -> 1677[label="",style="dashed", color="red", weight=0];
1320[label="primMinusNat Zero (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)))",fontsize=16,color="magenta"];1320 -> 1679[label="",style="dashed", color="magenta", weight=3];
1321 -> 1976[label="",style="dashed", color="red", weight=0];
1321[label="primPlusNat Zero (primDivNatS0 (Succ xz6100) (Succ xz630) (primGEqNatS xz6100 xz630))",fontsize=16,color="magenta"];1321 -> 1977[label="",style="dashed", color="magenta", weight=3];
1321 -> 1978[label="",style="dashed", color="magenta", weight=3];
1321 -> 1979[label="",style="dashed", color="magenta", weight=3];
1321 -> 1980[label="",style="dashed", color="magenta", weight=3];
1322[label="primPlusNat Zero (primDivNatS0 (Succ xz6100) Zero True)",fontsize=16,color="black",shape="box"];1322 -> 1333[label="",style="solid", color="black", weight=3];
1323[label="primPlusNat Zero (primDivNatS0 Zero (Succ xz630) False)",fontsize=16,color="black",shape="box"];1323 -> 1334[label="",style="solid", color="black", weight=3];
1324[label="primPlusNat Zero (primDivNatS0 Zero Zero True)",fontsize=16,color="black",shape="box"];1324 -> 1335[label="",style="solid", color="black", weight=3];
1912[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS (Succ xz960) xz97))",fontsize=16,color="burlywood",shape="box"];2480[label="xz97/Succ xz970",fontsize=10,color="white",style="solid",shape="box"];1912 -> 2480[label="",style="solid", color="burlywood", weight=9];
2480 -> 1926[label="",style="solid", color="burlywood", weight=3];
2481[label="xz97/Zero",fontsize=10,color="white",style="solid",shape="box"];1912 -> 2481[label="",style="solid", color="burlywood", weight=9];
2481 -> 1927[label="",style="solid", color="burlywood", weight=3];
1913[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS Zero xz97))",fontsize=16,color="burlywood",shape="box"];2482[label="xz97/Succ xz970",fontsize=10,color="white",style="solid",shape="box"];1913 -> 2482[label="",style="solid", color="burlywood", weight=9];
2482 -> 1928[label="",style="solid", color="burlywood", weight=3];
2483[label="xz97/Zero",fontsize=10,color="white",style="solid",shape="box"];1913 -> 2483[label="",style="solid", color="burlywood", weight=9];
2483 -> 1929[label="",style="solid", color="burlywood", weight=3];
1678 -> 2096[label="",style="dashed", color="red", weight=0];
1678[label="primDivNatS (primMinusNatS (Succ xz5700) Zero) (Succ Zero)",fontsize=16,color="magenta"];1678 -> 2097[label="",style="dashed", color="magenta", weight=3];
1678 -> 2098[label="",style="dashed", color="magenta", weight=3];
1678 -> 2099[label="",style="dashed", color="magenta", weight=3];
1677[label="primMinusNat Zero (Succ xz79)",fontsize=16,color="black",shape="triangle"];1677 -> 1693[label="",style="solid", color="black", weight=3];
1679 -> 2096[label="",style="dashed", color="red", weight=0];
1679[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];1679 -> 2100[label="",style="dashed", color="magenta", weight=3];
1679 -> 2101[label="",style="dashed", color="magenta", weight=3];
1679 -> 2102[label="",style="dashed", color="magenta", weight=3];
1977[label="xz6100",fontsize=16,color="green",shape="box"];1978[label="xz630",fontsize=16,color="green",shape="box"];1979[label="xz6100",fontsize=16,color="green",shape="box"];1980[label="xz630",fontsize=16,color="green",shape="box"];1976[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS xz109 xz110))",fontsize=16,color="burlywood",shape="triangle"];2486[label="xz109/Succ xz1090",fontsize=10,color="white",style="solid",shape="box"];1976 -> 2486[label="",style="solid", color="burlywood", weight=9];
2486 -> 2017[label="",style="solid", color="burlywood", weight=3];
2487[label="xz109/Zero",fontsize=10,color="white",style="solid",shape="box"];1976 -> 2487[label="",style="solid", color="burlywood", weight=9];
2487 -> 2018[label="",style="solid", color="burlywood", weight=3];
1333 -> 1741[label="",style="dashed", color="red", weight=0];
1333[label="primPlusNat Zero (Succ (primDivNatS (primMinusNatS (Succ xz6100) Zero) (Succ Zero)))",fontsize=16,color="magenta"];1333 -> 1742[label="",style="dashed", color="magenta", weight=3];
1334 -> 1300[label="",style="dashed", color="red", weight=0];
1334[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];1335 -> 1741[label="",style="dashed", color="red", weight=0];
1335[label="primPlusNat Zero (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)))",fontsize=16,color="magenta"];1335 -> 1743[label="",style="dashed", color="magenta", weight=3];
1926[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS (Succ xz960) (Succ xz970)))",fontsize=16,color="black",shape="box"];1926 -> 1943[label="",style="solid", color="black", weight=3];
1927[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS (Succ xz960) Zero))",fontsize=16,color="black",shape="box"];1927 -> 1944[label="",style="solid", color="black", weight=3];
1928[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS Zero (Succ xz970)))",fontsize=16,color="black",shape="box"];1928 -> 1945[label="",style="solid", color="black", weight=3];
1929[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];1929 -> 1946[label="",style="solid", color="black", weight=3];
2097[label="Zero",fontsize=16,color="green",shape="box"];2098[label="Zero",fontsize=16,color="green",shape="box"];2099[label="Succ xz5700",fontsize=16,color="green",shape="box"];2096[label="primDivNatS (primMinusNatS xz115 xz116) (Succ xz117)",fontsize=16,color="burlywood",shape="triangle"];2491[label="xz115/Succ xz1150",fontsize=10,color="white",style="solid",shape="box"];2096 -> 2491[label="",style="solid", color="burlywood", weight=9];
2491 -> 2148[label="",style="solid", color="burlywood", weight=3];
2492[label="xz115/Zero",fontsize=10,color="white",style="solid",shape="box"];2096 -> 2492[label="",style="solid", color="burlywood", weight=9];
2492 -> 2149[label="",style="solid", color="burlywood", weight=3];
1693[label="Neg (Succ xz79)",fontsize=16,color="green",shape="box"];2100[label="Zero",fontsize=16,color="green",shape="box"];2101[label="Zero",fontsize=16,color="green",shape="box"];2102[label="Zero",fontsize=16,color="green",shape="box"];2017[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS (Succ xz1090) xz110))",fontsize=16,color="burlywood",shape="box"];2493[label="xz110/Succ xz1100",fontsize=10,color="white",style="solid",shape="box"];2017 -> 2493[label="",style="solid", color="burlywood", weight=9];
2493 -> 2033[label="",style="solid", color="burlywood", weight=3];
2494[label="xz110/Zero",fontsize=10,color="white",style="solid",shape="box"];2017 -> 2494[label="",style="solid", color="burlywood", weight=9];
2494 -> 2034[label="",style="solid", color="burlywood", weight=3];
2018[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS Zero xz110))",fontsize=16,color="burlywood",shape="box"];2495[label="xz110/Succ xz1100",fontsize=10,color="white",style="solid",shape="box"];2018 -> 2495[label="",style="solid", color="burlywood", weight=9];
2495 -> 2035[label="",style="solid", color="burlywood", weight=3];
2496[label="xz110/Zero",fontsize=10,color="white",style="solid",shape="box"];2018 -> 2496[label="",style="solid", color="burlywood", weight=9];
2496 -> 2036[label="",style="solid", color="burlywood", weight=3];
1742 -> 2096[label="",style="dashed", color="red", weight=0];
1742[label="primDivNatS (primMinusNatS (Succ xz6100) Zero) (Succ Zero)",fontsize=16,color="magenta"];1742 -> 2109[label="",style="dashed", color="magenta", weight=3];
1742 -> 2110[label="",style="dashed", color="magenta", weight=3];
1742 -> 2111[label="",style="dashed", color="magenta", weight=3];
1741[label="primPlusNat Zero (Succ xz82)",fontsize=16,color="black",shape="triangle"];1741 -> 1757[label="",style="solid", color="black", weight=3];
1743 -> 2096[label="",style="dashed", color="red", weight=0];
1743[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];1743 -> 2112[label="",style="dashed", color="magenta", weight=3];
1743 -> 2113[label="",style="dashed", color="magenta", weight=3];
1743 -> 2114[label="",style="dashed", color="magenta", weight=3];
1943 -> 1871[label="",style="dashed", color="red", weight=0];
1943[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) (primGEqNatS xz960 xz970))",fontsize=16,color="magenta"];1943 -> 1961[label="",style="dashed", color="magenta", weight=3];
1943 -> 1962[label="",style="dashed", color="magenta", weight=3];
1944[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) True)",fontsize=16,color="black",shape="triangle"];1944 -> 1963[label="",style="solid", color="black", weight=3];
1945[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) False)",fontsize=16,color="black",shape="box"];1945 -> 1964[label="",style="solid", color="black", weight=3];
1946 -> 1944[label="",style="dashed", color="red", weight=0];
1946[label="primMinusNat Zero (primDivNatS0 (Succ xz94) (Succ xz95) True)",fontsize=16,color="magenta"];2148[label="primDivNatS (primMinusNatS (Succ xz1150) xz116) (Succ xz117)",fontsize=16,color="burlywood",shape="box"];2501[label="xz116/Succ xz1160",fontsize=10,color="white",style="solid",shape="box"];2148 -> 2501[label="",style="solid", color="burlywood", weight=9];
2501 -> 2150[label="",style="solid", color="burlywood", weight=3];
2502[label="xz116/Zero",fontsize=10,color="white",style="solid",shape="box"];2148 -> 2502[label="",style="solid", color="burlywood", weight=9];
2502 -> 2151[label="",style="solid", color="burlywood", weight=3];
2149[label="primDivNatS (primMinusNatS Zero xz116) (Succ xz117)",fontsize=16,color="burlywood",shape="box"];2503[label="xz116/Succ xz1160",fontsize=10,color="white",style="solid",shape="box"];2149 -> 2503[label="",style="solid", color="burlywood", weight=9];
2503 -> 2152[label="",style="solid", color="burlywood", weight=3];
2504[label="xz116/Zero",fontsize=10,color="white",style="solid",shape="box"];2149 -> 2504[label="",style="solid", color="burlywood", weight=9];
2504 -> 2153[label="",style="solid", color="burlywood", weight=3];
2033[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS (Succ xz1090) (Succ xz1100)))",fontsize=16,color="black",shape="box"];2033 -> 2046[label="",style="solid", color="black", weight=3];
2034[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS (Succ xz1090) Zero))",fontsize=16,color="black",shape="box"];2034 -> 2047[label="",style="solid", color="black", weight=3];
2035[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS Zero (Succ xz1100)))",fontsize=16,color="black",shape="box"];2035 -> 2048[label="",style="solid", color="black", weight=3];
2036[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];2036 -> 2049[label="",style="solid", color="black", weight=3];
2109[label="Zero",fontsize=16,color="green",shape="box"];2110[label="Zero",fontsize=16,color="green",shape="box"];2111[label="Succ xz6100",fontsize=16,color="green",shape="box"];1757[label="Succ xz82",fontsize=16,color="green",shape="box"];2112[label="Zero",fontsize=16,color="green",shape="box"];2113[label="Zero",fontsize=16,color="green",shape="box"];2114[label="Zero",fontsize=16,color="green",shape="box"];1961[label="xz960",fontsize=16,color="green",shape="box"];1962[label="xz970",fontsize=16,color="green",shape="box"];1963 -> 1677[label="",style="dashed", color="red", weight=0];
1963[label="primMinusNat Zero (Succ (primDivNatS (primMinusNatS (Succ xz94) (Succ xz95)) (Succ (Succ xz95))))",fontsize=16,color="magenta"];1963 -> 2019[label="",style="dashed", color="magenta", weight=3];
1964 -> 1289[label="",style="dashed", color="red", weight=0];
1964[label="primMinusNat Zero Zero",fontsize=16,color="magenta"];2150[label="primDivNatS (primMinusNatS (Succ xz1150) (Succ xz1160)) (Succ xz117)",fontsize=16,color="black",shape="box"];2150 -> 2154[label="",style="solid", color="black", weight=3];
2151[label="primDivNatS (primMinusNatS (Succ xz1150) Zero) (Succ xz117)",fontsize=16,color="black",shape="box"];2151 -> 2155[label="",style="solid", color="black", weight=3];
2152[label="primDivNatS (primMinusNatS Zero (Succ xz1160)) (Succ xz117)",fontsize=16,color="black",shape="box"];2152 -> 2156[label="",style="solid", color="black", weight=3];
2153[label="primDivNatS (primMinusNatS Zero Zero) (Succ xz117)",fontsize=16,color="black",shape="box"];2153 -> 2157[label="",style="solid", color="black", weight=3];
2046 -> 1976[label="",style="dashed", color="red", weight=0];
2046[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) (primGEqNatS xz1090 xz1100))",fontsize=16,color="magenta"];2046 -> 2056[label="",style="dashed", color="magenta", weight=3];
2046 -> 2057[label="",style="dashed", color="magenta", weight=3];
2047[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) True)",fontsize=16,color="black",shape="triangle"];2047 -> 2058[label="",style="solid", color="black", weight=3];
2048[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) False)",fontsize=16,color="black",shape="box"];2048 -> 2059[label="",style="solid", color="black", weight=3];
2049 -> 2047[label="",style="dashed", color="red", weight=0];
2049[label="primPlusNat Zero (primDivNatS0 (Succ xz107) (Succ xz108) True)",fontsize=16,color="magenta"];2019 -> 2096[label="",style="dashed", color="red", weight=0];
2019[label="primDivNatS (primMinusNatS (Succ xz94) (Succ xz95)) (Succ (Succ xz95))",fontsize=16,color="magenta"];2019 -> 2118[label="",style="dashed", color="magenta", weight=3];
2019 -> 2119[label="",style="dashed", color="magenta", weight=3];
2019 -> 2120[label="",style="dashed", color="magenta", weight=3];
2154 -> 2096[label="",style="dashed", color="red", weight=0];
2154[label="primDivNatS (primMinusNatS xz1150 xz1160) (Succ xz117)",fontsize=16,color="magenta"];2154 -> 2158[label="",style="dashed", color="magenta", weight=3];
2154 -> 2159[label="",style="dashed", color="magenta", weight=3];
2155[label="primDivNatS (Succ xz1150) (Succ xz117)",fontsize=16,color="black",shape="box"];2155 -> 2160[label="",style="solid", color="black", weight=3];
2156[label="primDivNatS Zero (Succ xz117)",fontsize=16,color="black",shape="triangle"];2156 -> 2161[label="",style="solid", color="black", weight=3];
2157 -> 2156[label="",style="dashed", color="red", weight=0];
2157[label="primDivNatS Zero (Succ xz117)",fontsize=16,color="magenta"];2056[label="xz1090",fontsize=16,color="green",shape="box"];2057[label="xz1100",fontsize=16,color="green",shape="box"];2058 -> 1741[label="",style="dashed", color="red", weight=0];
2058[label="primPlusNat Zero (Succ (primDivNatS (primMinusNatS (Succ xz107) (Succ xz108)) (Succ (Succ xz108))))",fontsize=16,color="magenta"];2058 -> 2070[label="",style="dashed", color="magenta", weight=3];
2059 -> 1300[label="",style="dashed", color="red", weight=0];
2059[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];2118[label="Succ xz95",fontsize=16,color="green",shape="box"];2119[label="Succ xz95",fontsize=16,color="green",shape="box"];2120[label="Succ xz94",fontsize=16,color="green",shape="box"];2158[label="xz1160",fontsize=16,color="green",shape="box"];2159[label="xz1150",fontsize=16,color="green",shape="box"];2160[label="primDivNatS0 xz1150 xz117 (primGEqNatS xz1150 xz117)",fontsize=16,color="burlywood",shape="box"];2514[label="xz1150/Succ xz11500",fontsize=10,color="white",style="solid",shape="box"];2160 -> 2514[label="",style="solid", color="burlywood", weight=9];
2514 -> 2162[label="",style="solid", color="burlywood", weight=3];
2515[label="xz1150/Zero",fontsize=10,color="white",style="solid",shape="box"];2160 -> 2515[label="",style="solid", color="burlywood", weight=9];
2515 -> 2163[label="",style="solid", color="burlywood", weight=3];
2161[label="Zero",fontsize=16,color="green",shape="box"];2070 -> 2096[label="",style="dashed", color="red", weight=0];
2070[label="primDivNatS (primMinusNatS (Succ xz107) (Succ xz108)) (Succ (Succ xz108))",fontsize=16,color="magenta"];2070 -> 2121[label="",style="dashed", color="magenta", weight=3];
2070 -> 2122[label="",style="dashed", color="magenta", weight=3];
2070 -> 2123[label="",style="dashed", color="magenta", weight=3];
2162[label="primDivNatS0 (Succ xz11500) xz117 (primGEqNatS (Succ xz11500) xz117)",fontsize=16,color="burlywood",shape="box"];2517[label="xz117/Succ xz1170",fontsize=10,color="white",style="solid",shape="box"];2162 -> 2517[label="",style="solid", color="burlywood", weight=9];
2517 -> 2164[label="",style="solid", color="burlywood", weight=3];
2518[label="xz117/Zero",fontsize=10,color="white",style="solid",shape="box"];2162 -> 2518[label="",style="solid", color="burlywood", weight=9];
2518 -> 2165[label="",style="solid", color="burlywood", weight=3];
2163[label="primDivNatS0 Zero xz117 (primGEqNatS Zero xz117)",fontsize=16,color="burlywood",shape="box"];2519[label="xz117/Succ xz1170",fontsize=10,color="white",style="solid",shape="box"];2163 -> 2519[label="",style="solid", color="burlywood", weight=9];
2519 -> 2166[label="",style="solid", color="burlywood", weight=3];
2520[label="xz117/Zero",fontsize=10,color="white",style="solid",shape="box"];2163 -> 2520[label="",style="solid", color="burlywood", weight=9];
2520 -> 2167[label="",style="solid", color="burlywood", weight=3];
2121[label="Succ xz108",fontsize=16,color="green",shape="box"];2122[label="Succ xz108",fontsize=16,color="green",shape="box"];2123[label="Succ xz107",fontsize=16,color="green",shape="box"];2164[label="primDivNatS0 (Succ xz11500) (Succ xz1170) (primGEqNatS (Succ xz11500) (Succ xz1170))",fontsize=16,color="black",shape="box"];2164 -> 2168[label="",style="solid", color="black", weight=3];
2165[label="primDivNatS0 (Succ xz11500) Zero (primGEqNatS (Succ xz11500) Zero)",fontsize=16,color="black",shape="box"];2165 -> 2169[label="",style="solid", color="black", weight=3];
2166[label="primDivNatS0 Zero (Succ xz1170) (primGEqNatS Zero (Succ xz1170))",fontsize=16,color="black",shape="box"];2166 -> 2170[label="",style="solid", color="black", weight=3];
2167[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];2167 -> 2171[label="",style="solid", color="black", weight=3];
2168 -> 2330[label="",style="dashed", color="red", weight=0];
2168[label="primDivNatS0 (Succ xz11500) (Succ xz1170) (primGEqNatS xz11500 xz1170)",fontsize=16,color="magenta"];2168 -> 2331[label="",style="dashed", color="magenta", weight=3];
2168 -> 2332[label="",style="dashed", color="magenta", weight=3];
2168 -> 2333[label="",style="dashed", color="magenta", weight=3];
2168 -> 2334[label="",style="dashed", color="magenta", weight=3];
2169[label="primDivNatS0 (Succ xz11500) Zero True",fontsize=16,color="black",shape="box"];2169 -> 2174[label="",style="solid", color="black", weight=3];
2170[label="primDivNatS0 Zero (Succ xz1170) False",fontsize=16,color="black",shape="box"];2170 -> 2175[label="",style="solid", color="black", weight=3];
2171[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];2171 -> 2176[label="",style="solid", color="black", weight=3];
2331[label="xz11500",fontsize=16,color="green",shape="box"];2332[label="xz1170",fontsize=16,color="green",shape="box"];2333[label="xz1170",fontsize=16,color="green",shape="box"];2334[label="xz11500",fontsize=16,color="green",shape="box"];2330[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS xz136 xz137)",fontsize=16,color="burlywood",shape="triangle"];2522[label="xz136/Succ xz1360",fontsize=10,color="white",style="solid",shape="box"];2330 -> 2522[label="",style="solid", color="burlywood", weight=9];
2522 -> 2363[label="",style="solid", color="burlywood", weight=3];
2523[label="xz136/Zero",fontsize=10,color="white",style="solid",shape="box"];2330 -> 2523[label="",style="solid", color="burlywood", weight=9];
2523 -> 2364[label="",style="solid", color="burlywood", weight=3];
2174[label="Succ (primDivNatS (primMinusNatS (Succ xz11500) Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];2174 -> 2181[label="",style="dashed", color="green", weight=3];
2175[label="Zero",fontsize=16,color="green",shape="box"];2176[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];2176 -> 2182[label="",style="dashed", color="green", weight=3];
2363[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS (Succ xz1360) xz137)",fontsize=16,color="burlywood",shape="box"];2524[label="xz137/Succ xz1370",fontsize=10,color="white",style="solid",shape="box"];2363 -> 2524[label="",style="solid", color="burlywood", weight=9];
2524 -> 2365[label="",style="solid", color="burlywood", weight=3];
2525[label="xz137/Zero",fontsize=10,color="white",style="solid",shape="box"];2363 -> 2525[label="",style="solid", color="burlywood", weight=9];
2525 -> 2366[label="",style="solid", color="burlywood", weight=3];
2364[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS Zero xz137)",fontsize=16,color="burlywood",shape="box"];2526[label="xz137/Succ xz1370",fontsize=10,color="white",style="solid",shape="box"];2364 -> 2526[label="",style="solid", color="burlywood", weight=9];
2526 -> 2367[label="",style="solid", color="burlywood", weight=3];
2527[label="xz137/Zero",fontsize=10,color="white",style="solid",shape="box"];2364 -> 2527[label="",style="solid", color="burlywood", weight=9];
2527 -> 2368[label="",style="solid", color="burlywood", weight=3];
2181 -> 2096[label="",style="dashed", color="red", weight=0];
2181[label="primDivNatS (primMinusNatS (Succ xz11500) Zero) (Succ Zero)",fontsize=16,color="magenta"];2181 -> 2187[label="",style="dashed", color="magenta", weight=3];
2181 -> 2188[label="",style="dashed", color="magenta", weight=3];
2181 -> 2189[label="",style="dashed", color="magenta", weight=3];
2182 -> 2096[label="",style="dashed", color="red", weight=0];
2182[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];2182 -> 2190[label="",style="dashed", color="magenta", weight=3];
2182 -> 2191[label="",style="dashed", color="magenta", weight=3];
2182 -> 2192[label="",style="dashed", color="magenta", weight=3];
2365[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS (Succ xz1360) (Succ xz1370))",fontsize=16,color="black",shape="box"];2365 -> 2369[label="",style="solid", color="black", weight=3];
2366[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS (Succ xz1360) Zero)",fontsize=16,color="black",shape="box"];2366 -> 2370[label="",style="solid", color="black", weight=3];
2367[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS Zero (Succ xz1370))",fontsize=16,color="black",shape="box"];2367 -> 2371[label="",style="solid", color="black", weight=3];
2368[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];2368 -> 2372[label="",style="solid", color="black", weight=3];
2187[label="Zero",fontsize=16,color="green",shape="box"];2188[label="Zero",fontsize=16,color="green",shape="box"];2189[label="Succ xz11500",fontsize=16,color="green",shape="box"];2190[label="Zero",fontsize=16,color="green",shape="box"];2191[label="Zero",fontsize=16,color="green",shape="box"];2192[label="Zero",fontsize=16,color="green",shape="box"];2369 -> 2330[label="",style="dashed", color="red", weight=0];
2369[label="primDivNatS0 (Succ xz134) (Succ xz135) (primGEqNatS xz1360 xz1370)",fontsize=16,color="magenta"];2369 -> 2373[label="",style="dashed", color="magenta", weight=3];
2369 -> 2374[label="",style="dashed", color="magenta", weight=3];
2370[label="primDivNatS0 (Succ xz134) (Succ xz135) True",fontsize=16,color="black",shape="triangle"];2370 -> 2375[label="",style="solid", color="black", weight=3];
2371[label="primDivNatS0 (Succ xz134) (Succ xz135) False",fontsize=16,color="black",shape="box"];2371 -> 2376[label="",style="solid", color="black", weight=3];
2372 -> 2370[label="",style="dashed", color="red", weight=0];
2372[label="primDivNatS0 (Succ xz134) (Succ xz135) True",fontsize=16,color="magenta"];2373[label="xz1370",fontsize=16,color="green",shape="box"];2374[label="xz1360",fontsize=16,color="green",shape="box"];2375[label="Succ (primDivNatS (primMinusNatS (Succ xz134) (Succ xz135)) (Succ (Succ xz135)))",fontsize=16,color="green",shape="box"];2375 -> 2377[label="",style="dashed", color="green", weight=3];
2376[label="Zero",fontsize=16,color="green",shape="box"];2377 -> 2096[label="",style="dashed", color="red", weight=0];
2377[label="primDivNatS (primMinusNatS (Succ xz134) (Succ xz135)) (Succ (Succ xz135))",fontsize=16,color="magenta"];2377 -> 2378[label="",style="dashed", color="magenta", weight=3];
2377 -> 2379[label="",style="dashed", color="magenta", weight=3];
2377 -> 2380[label="",style="dashed", color="magenta", weight=3];
2378[label="Succ xz135",fontsize=16,color="green",shape="box"];2379[label="Succ xz135",fontsize=16,color="green",shape="box"];2380[label="Succ xz134",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xz134, xz135, Zero, Zero) → new_primDivNatS00(xz134, xz135)
new_primDivNatS0(xz134, xz135, Succ(xz1360), Succ(xz1370)) → new_primDivNatS0(xz134, xz135, xz1360, xz1370)
new_primDivNatS(Succ(xz1150), Succ(xz1160), xz117) → new_primDivNatS(xz1150, xz1160, xz117)
new_primDivNatS(Succ(Succ(xz11500)), Zero, Succ(xz1170)) → new_primDivNatS0(xz11500, xz1170, xz11500, xz1170)
new_primDivNatS(Succ(Zero), Zero, Zero) → new_primDivNatS(Zero, Zero, Zero)
new_primDivNatS(Succ(Succ(xz11500)), Zero, Zero) → new_primDivNatS(Succ(xz11500), Zero, Zero)
new_primDivNatS00(xz134, xz135) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))
new_primDivNatS0(xz134, xz135, Succ(xz1360), Zero) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ QDPSizeChangeProof

                                    ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(xz11500)), Zero, Zero) → new_primDivNatS(Succ(xz11500), Zero, Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS(Succ(Succ(xz11500)), Zero, Zero) → new_primDivNatS(Succ(xz11500), Zero, Zero)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 2, 2 >= 3, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPOrderProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xz134, xz135, Zero, Zero) → new_primDivNatS00(xz134, xz135)
new_primDivNatS0(xz134, xz135, Succ(xz1360), Succ(xz1370)) → new_primDivNatS0(xz134, xz135, xz1360, xz1370)
new_primDivNatS(Succ(xz1150), Succ(xz1160), xz117) → new_primDivNatS(xz1150, xz1160, xz117)
new_primDivNatS(Succ(Succ(xz11500)), Zero, Succ(xz1170)) → new_primDivNatS0(xz11500, xz1170, xz11500, xz1170)
new_primDivNatS00(xz134, xz135) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))
new_primDivNatS0(xz134, xz135, Succ(xz1360), Zero) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS(Succ(xz1150), Succ(xz1160), xz117) → new_primDivNatS(xz1150, xz1160, xz117)
new_primDivNatS(Succ(Succ(xz11500)), Zero, Succ(xz1170)) → new_primDivNatS0(xz11500, xz1170, xz11500, xz1170)

The remaining pairs can at least be oriented weakly.

new_primDivNatS0(xz134, xz135, Zero, Zero) → new_primDivNatS00(xz134, xz135)
new_primDivNatS0(xz134, xz135, Succ(xz1360), Succ(xz1370)) → new_primDivNatS0(xz134, xz135, xz1360, xz1370)
new_primDivNatS00(xz134, xz135) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))
new_primDivNatS0(xz134, xz135, Succ(xz1360), Zero) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂, x₃)) = x₁
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = 1 + x₁
POL(new_primDivNatS00(x₁, x₂)) = 1 + x₁

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xz134, xz135, Zero, Zero) → new_primDivNatS00(xz134, xz135)
new_primDivNatS0(xz134, xz135, Succ(xz1360), Succ(xz1370)) → new_primDivNatS0(xz134, xz135, xz1360, xz1370)
new_primDivNatS00(xz134, xz135) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))
new_primDivNatS0(xz134, xz135, Succ(xz1360), Zero) → new_primDivNatS(Succ(xz134), Succ(xz135), Succ(xz135))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xz134, xz135, Succ(xz1360), Succ(xz1370)) → new_primDivNatS0(xz134, xz135, xz1360, xz1370)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(xz134, xz135, Succ(xz1360), Succ(xz1370)) → new_primDivNatS0(xz134, xz135, xz1360, xz1370)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(xz94, xz95, Succ(xz960), Succ(xz970)) → new_primMinusNat(xz94, xz95, xz960, xz970)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(xz94, xz95, Succ(xz960), Succ(xz970)) → new_primMinusNat(xz94, xz95, xz960, xz970)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat0(Succ(xz570), Succ(xz580), xz59) → new_primMinusNat0(xz570, xz580, xz59)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat0(Succ(xz570), Succ(xz580), xz59) → new_primMinusNat0(xz570, xz580, xz59)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat1(xz45, xz46, Succ(xz470), Succ(xz480)) → new_primMinusNat1(xz45, xz46, xz470, xz480)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat1(xz45, xz46, Succ(xz470), Succ(xz480)) → new_primMinusNat1(xz45, xz46, xz470, xz480)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(xz107, xz108, Succ(xz1090), Succ(xz1100)) → new_primPlusNat(xz107, xz108, xz1090, xz1100)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(xz107, xz108, Succ(xz1090), Succ(xz1100)) → new_primPlusNat(xz107, xz108, xz1090, xz1100)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat0(Succ(xz610), Succ(xz620), xz63) → new_primPlusNat0(xz610, xz620, xz63)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat0(Succ(xz610), Succ(xz620), xz63) → new_primPlusNat0(xz610, xz620, xz63)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat1(xz50, xz51, Succ(xz520), Succ(xz530)) → new_primPlusNat1(xz50, xz51, xz520, xz530)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat1(xz50, xz51, Succ(xz520), Succ(xz530)) → new_primPlusNat1(xz50, xz51, xz520, xz530)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x